package ewu

import gui.Layout
import java.util.ArrayList
import scala.collection.mutable.ArrayBuffer
import ewu._
import scala.swing._
import scala.swing.Dialog._
import scala.io._

/**
 * Diese von der Klasse Anweisung abgeleitete Klasse stellt Zusicherungen dar.
 * Hierzu gibt es einen Bezeichner "prefix" sowie den boolschen Ausdruck "expr"
 * fuer die Zusicherungsbedingung.
 */

case class Assertion (prefix: String, expr: BoolExpression) extends Anweisung {

  override def numerate(num: List[Int]) = null
  
  override def tabbate(i: Int) = {
    tabs = i
  }

  override def propagate(assV: Anweisung, assN: Anweisung): Anweisungsfolge = null

  override def propagate(assI: Anweisung): Anweisungsfolge = null

  override def trace(env: Environment, aenv: ArrayEnvironment, tt: Layout, h: Int):
                                                                (String, Boolean, Int) = {
    var ausgabe: String = "--#"
    if(!prefix.equals(""))
      ausgabe ++= prefix ++ ": "
    ausgabe ++= expr + " => "

    if(expr.evaluate(env) == Some(true))
      ausgabe ++= "true"
    else 
      ausgabe ++= "false"

    return (ausgabe ++ "\n", expr.evaluate(env) == Some(true), h+1)
  }

  def evaluate (env: Environment): Option[Boolean] =
    expr.evaluate(env)

  override def toString: String = {
    var ausgabe: String = "--#"
    ausgabe ++= prefix ++ ": "
    ausgabe ++= expr + "\n"
    return ausgabe
  }
  
  override def toTabString: String = {
    var ausgabe: String = HM.tabString(tabs)
    ausgabe ++= "--#"
    ausgabe ++= prefix ++ ": "
    ausgabe ++= expr + "\n"
    return ausgabe
  }
  
  def toCheckVersion(addfuncs: ArrayList[String], arrayvars: ArrayList[String]) : (Anweisung, Anweisungsfolge) = {
    var anwfolge = new Anweisungsfolge(new ArrayBuffer())
    var elset = new Anweisungsfolge(new ArrayBuffer())
    elset.addAnweisung(Text("put_line(\"" + expr + " => false\");"))
    return (new Fall(expr.replaceQuantor(addfuncs, arrayvars), anwfolge, elset), anwfolge)
  }

  private def tab (t: Int): String = {
    if (t > 0)
      " " + tab(t-1)
    else
      ""
  }

  def reduce: Assertion = Assertion(prefix, expr.reduce)
  
  def getVariables(a: ArrayBuffer[Name]) = {
    expr.getVariables(a)
  }
  
  def replaceVariable(fromVar: Name, toVar: Expression) : Unit = {
    expr.replaceVariable(fromVar, toVar)
  }
  
}


 